Inverse Image (Rank) Induction lemmas and tactics
=================================================
inv_image_ind_a: The basic lemma. Read this to understand proof method
inv_image_ind_tp: A template proof for the InvImageInd tactic
inv_image_ind_tac: Definition of the InvImageInd tactic
rank_ind_tac: Definition of RankInd tactic.
rank_ind_tac: DeOften more convenient than InvImageInd
inv_image_ind: Test of InvImageInd tactic